Use temporary variable to initialise array cells #4523
Conversation
smowton
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli and
thk123
as code owners
smowton
force-pushed
the
smowton/feature/use-temporary-to-init-multidimensional-array
branch
from
aeb4a5f to
88a05eb
Compare
| else | ||
| { | ||
| init_expr = allocate_objects.allocate_automatic_local_object( | ||
| arraycellref.type(), "new_array_item"); |
There was a problem hiding this comment.
Please use the same name as in the comment above (either this to new_item, or the comment to new_array_item
| // alias, cf. the harder-to-analyse | ||
| // `some_expr[idx]->x = y; some_expr[idx]->z = w;` | ||
| exprt init_expr; | ||
| if(new_item_is_primitive) |
There was a problem hiding this comment.
💡 Any reason to not to do the primitives in the same way, just in the interest of keeping this code simpler?
There was a problem hiding this comment.
Just to keep it simple indeed. array[idx] = nondet(int) -> new_array_item = nondet(int); array[idx] = new_array_item; seems like a disservice to the reader.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 88a05eb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108119473
Previously when dealing with multidimensional arrays we could end up generating expressions such as array[idx] = ALLOCATE Something; array[idx]->field1 = x; array[idx]->field2 = y; This was a struggle for symex, as every reference to array[idx] could be a bad dereference, and so symex::invalid_object (or perhaps some_symbol$object) references were created to account for this possiblity. By using a temporary (generating code like `t = ALLOCATE Something; t->field1 = x; t->field2 = y; array[idx] = t;`) it is much clearer that the pointer dereferences must refer to the newly allocated object, and so the problematic case is avoided.
smowton
force-pushed
the
smowton/feature/use-temporary-to-init-multidimensional-array
branch
from
88a05eb to
703e7c1
Compare
|
Oops, I wrote a test then forgot to commit it, added now. |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 703e7c1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108129000
Previously when dealing with multidimensional arrays we could end up generating expressions
such as array[idx] = ALLOCATE Something; array[idx]->field1 = x; array[idx]->field2 = y;
This was a struggle for symex, as every reference to array[idx] could be a bad dereference,
and so symex::invalid_object (or perhaps some_symbol$object) references were created to account
for this possiblity. By using a temporary (generating code like
t = ALLOCATE Something; t->field1 = x; t->field2 = y; array[idx] = t;) it is much clearerthat the pointer dereferences must refer to the newly allocated object, and so the problematic
case is avoided.